#include <stdio.h>
#include <stddef.h>
#include <stdlib.h>
#include <string.h>

#define FACTOR 100


main(int argc, char **argv)
{

  int i,j;

  int numvar,numdata;

  char *buf=NULL;
  int lenbuf;

  char var[100][100]; //variables cant be more than 100 long
  float data[10000][100]; //only 10000 data points allowed of 100 variables
  
  float max; //maximum time value

  char tok[1000];
  char cmd[1000];
   int out;
  FILE *fp;


  //check if we got three arguments
  if(argc<3)
    {
      printf("Expected three arguments - Simulation data file, TCTL Property\n.");
      exit(-1);

    }

  fp = fopen(argv[1],"r");
  if(fp==NULL)
    {
      printf("Error opening file %s with simulation data.\n",argv[1]);
      exit(-1);
    }

  //read and dump the first #

  fscanf(fp," %s ", tok);

  if(tok[0]!='#')
    {
      printf("Simulation data file must begin with #\n");
      exit(-1);
    }

  //count the variable names
  i=0;
  do
    {
      fscanf(fp," %s ",var[i]);
      i++;
    }
  while(strlen(var[i-1]) != strspn(var[i-1],"0123456789.e+-"));

  numvar = i-1; //counted the number of variables

  i=0;
  fclose(fp);



  //count length of data file
 fp = fopen(argv[1],"r");
  if(fp==NULL)
    {
      printf("Error opening file %s with simulation data.\n",argv[1]);
      exit(-1);
    }

  i=0;
  while(getline(&buf,&lenbuf,fp)!=-1)
    {
      i++; printf("Line %d: %s\n",i-1,buf);
    }
  numdata=i-1;


  i=0;
  fclose(fp);

  //numvar = strtod(argv[2], NULL); //number of variables
  //numdata = strtod(argv[3], NULL); //number of data points

  printf ("\nExpecting data file with %d variables and time series of length %d \n\n",numvar,numdata);


  
  fp = fopen(argv[1],"r");
  if(fp==NULL)
    {
      printf("Error opening file %s with simulation data.\n",argv[1]);
      exit(-1);
    }


  //read and dump the first #

  fscanf(fp," %s ", tok);

  if(tok[0]!='#')
    {
      printf("Simulation data file must begin with #\n");
      exit(-1);
    }


  //ready to read the variable names
  for(i=0;i<numvar;i++)
    {
      fscanf(fp," %s ",var[i]);
    }


  //check if time is present and subsitute by duration

  if(strcmp(var[0],"time"))
    {
      printf("First variable must be time\n");
      exit(-1);
    }
  else
    {
      strcpy(var[0],"duration"); 
    }

 //ready to read the variable values
  max = -1;
  for(j=0;j<numdata;j++)
    {
      for(i=0;i<numvar;i++)
	{
	  fscanf(fp," %f ",&data[j][i]);
	 
	}
       if(max < data[j][0])
	    {
	      max = data[j][0];
	    }
    }

  
  //all data read
  //close file
  fclose(fp);

  printf("Input file read. Generating output file\n");
  //compute maximum of each data point

  

  //start writing to TSMV file

  fp = fopen("data.smv","w");

  if(fp==NULL)
    {
      printf("Unable to open output file\n");
      exit(-1);
    }
  

  fprintf(fp, "MODULE main \n\n\n\n");

  fprintf(fp, "VAR \n");


  //ready to print the first variable name
  for(i=0;i<1;i++)
    {
      fprintf(fp,"%s: 0..%d; \n",var[i],(int)(max*FACTOR));//2D precision
    }


  //initialize time in model to 0
  fprintf(fp,"\n\n\n\nINIT \n  duration=1\n\n\n\n");


  printf("\nNow printing definitions.....\n");
  //each pair of time steps defines the variable values
  fprintf(fp, "\n\n\n\nDEFINE \n");

  for(i=1;i<numvar;i++) //for each variable in trace
    {

      fprintf(fp,"\n %s := \n   case \n", var[i]);
      for(j=0;j<numdata;j++) //for each data point
	{
	  if(j<=numdata-2)
	    {
	      fprintf(fp, "duration >= %d & duration<%d  \t : %d;\n",(int)(data[j][0]*FACTOR),(int)(data[j+1][0]*FACTOR),(int)(data[j][i]));
	    }
	  else
	    {
	      fprintf(fp, "duration >= %d \t : %d;\n",(int)(data[j][0]*FACTOR),(int)(data[j][i]));
	    }
	}

      fprintf(fp,"\t\t esac; \n\n");

    }



  //only time should evolve
  fprintf(fp,"\n\nTRANS\n  next(duration mod 1 = 0)\n");

  fprintf(fp, "\n\n SPEC\n  %s \n ",argv[2]);


  fclose(fp);


  //printed the smv file
  //ask TSMV to simulate it

  sprintf(cmd,"./TSMV data.smv > temp.out");
  out = system(cmd);
  if (out!=0)
    {
      printf("Sorry! The input TCTL formula may not be correct.1\n");
      while(1);
    }
  else
    {
      out=system("grep \"true\" temp.out | wc -l > decision");
      out=system("grep \"false\" temp.out | wc -l > decision1");
      fp = fopen("decision","r");
      if (fp==NULL)
	{
	  printf("Sorry! The input TCTL formula may not be correct.2\n");
	  while(1);
	}

      fscanf(fp," %d ", &out);
      fclose(fp);
      if(out==1)
	return(1);
      
      fp = fopen("decision1","r");
      if (fp==NULL)
	{
	  printf("Sorry! The input TCTL formula may not be correct. 3\n");
	  while(1);
	}

      fscanf(fp," %d ", &out);
      fclose(fp);
      if(out==1)
	return(0);


      printf("Sorry! The input TCTL formula may not be correct.4\n");
      while(1);
      

    }
}
